es:ES, A:Type, i:Id, ds:x:Id fp Type, conds:k:Knd fp V:Type  (State(ds)V(A + Top)).
(e:E.
(loc(e) = i)
 (kind(e)  dom(conds))
 ((valtype(e) r (conds(kind(e)).1)) & (state@loc(e) r State(ds))))
 (e:E.
 ((e  es-triggers(es;i;ds;conds)))
  (loc(e) = i & (kind(e)  fpf-domain(conds))
  & (isl((conds(kind(e)).2)((state when e),val(e)))))) 

latex

Definitions

valtype(e), Type, State(ds), Top, left + right, x:AB(x), Knd, x:A  B(x), f(x), t.1, t  T, val(e), x:A. B(x), P  Q, state@i, (state when e), b, isl(x), , ff, (x  l), <a, b>, Id, s = t, P  Q, x. t(x), x.A(x), t.2, f(a), , fpf-domain(f), P & Q, P  Q, P  Q, a:A fp B(a), A, True, b, p q, T, Unit, can-apply(f;x), e  X, es-triggers(es;i;ds;conds), ES, E, loc(e), a = b, kind(e), KindDeq, x  dom(f), p  q, Atom$n, a < b, vartype(i;x), f(x)?z, IdDeq, @i discrete ds, {T}, SQType(T), tt, let x,y = A in B(x;y), {x:A| B(x)} , type List, False, case b of inl(x) => s(x) | inr(y) => t(y), A c B, IdLnk, if b then t else f fi , Void

Lemmas

member-fpf-domain, IdLnk wf, false wf, btrue wf, bfalse wf, es-state-subtype2, es-state-subtype, fpf-cap wf, id-deq wf, es-state-subtype-iff, member-fpf-dom, es-E wf, es-valtype wf, pi1 wf, es-state wf, Knd wf, fpf wf, Id wf, event system wf, eqtt to assert, assert of band, and functionality wrt iff, eqff to assert, squash wf, true wf, bnot thru band, assert of bor, or functionality wrt iff, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bor wf, bnot wf, not wf, band wf, fpf-dom wf, Kind-deq wf, es-kind wf, eq id wf, es-loc wf, fpf-trivial-subtype-top, bool wf, l member wf, fpf-domain wf, assert wf, isl wf, top wf, pi2 wf, decl-state wf, fpf-ap wf, es-state-when wf, es-val wf